Nuprl Lemma : prop_and_wf
4,23
postcript
pdf
T
:Type,
P
,
Q
:(
T
Prop). (
P
Q
)
T
Prop
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Prop
,
t
T
origin
T:Type, P, Q:(T
Prop). (P 
Q) 
TProp T:Type, P, Q:(TProp). (P Q) TProp Qx:A. B(x) T